Step of Proof: mul_bounds_1b
12,41
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
mul
bounds
1b
:
.....assertion..... NILNIL
1.
a
:
2.
b
:
(
a
* 0) < (
a
*
b
)
latex
by ((BackThruLemma `mul_preserves_lt`)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C
),(first_nat 3:n)) (first_tok :t) inil_term)))
latex
C
.
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
mul
preserves
lt
origin